perm filename PCHECK[CHE,WD]2 blob
sn#017523 filedate 1972-12-23 generic text, type T, neo UTF8
00100 REMPROP('MAP,'NEWFORM);
00200 REMPROP('MAPLIST,'NEWFORM);
00300 REMPROP('MAPCAR,'NEWFORM);
00400
00500 REMPROP('EXPLODE,'NEWNAM);
00600 REMPROP('LC,'NEWNAM);
00700
00800 PUTPROP('!≥,'(NIL GEQ NIL),'SWITCH!*);
00900 PUTPROP('!≤,'(NIL LEQ NIL),'SWITCH!*);
01000 PUTPROP('!≠,'(NIL NEQ NIL),'SWITCH!*);
01100
01200 PUTPROP('EXPR,'PROCSTAT,'STAT);
01300
01400 IF CDR GET('!*TRANS,'VALUE)=T
01500 THEN BEGIN OUT(PCHECK.LSP); OFF NOPOINT; ON DEFN; END
01600 ELSE PUTPROP('SHUT,
01700 '(LAMBDA (L) (REMPROP (QUOTE SHUT) (QUOTE EXPR))),
01800 'EXPR);
01900
02000 DECLARE(DECIMAL(),
02100 SPECIAL(AXIOMS,CURLIN,CURPRF,PROOFS,SCHEMAS,THEOREMS),
02200 SPECIAL(LOGICALCONSTANTS,QUANTIFIERS),
02300 SPECIAL(EXPEXP,EXPLGTH,EXPLIM,ORDCNT),
02400 SPECIAL(CONSOLEWIDTH,DDWIDTH,FILEWIDTH,IIIWIDTH,
02500 IMLACWIDTH,TTYWIDTH),
02600 SPECIAL(!*FILEPRINT,PRECLIS!*,!*PRINT,!*TWODIM));
02700
00100 %PROPERTY TABLE MANIPULATION PRIMITIVES%
00200
00300 MACRO FIRSTPROP L; 'CDR.CDR L;
00400
00500 MACRO LASTPROP L; 'NULL.CDR L;
00600
00700 MACRO NEXTPROP L; 'CDDR.CDR L;
00800
00900 MACRO PROPNAM L; 'CAR.CDR L;
01000
01100 MACRO PROPTABLE L; 'CDR.CDR L;
01200
01300 MACRO PROPVAL L; 'CADR.CDR L;
01400
01500 EXPR DELETEPROP(IDENT,PROPNAM);
01600 BEGIN SCALAR TEM;
01700 TEM←IDENT;
01800 LOOP: IF NULL CDR TEM THEN RETURN;
01900 IF CADR TEM EQ PROPNAM THEN RETURN PROG2(RPLACD(TEM,CDDDR TEM),T);
02000 TEM←CDDR TEM;
02100 GO LOOP;
02200 END;
02300
02400 EXPR GETGET(ATOM,PROP);
02500 BEGIN SCALAR TEM,PTAB;
02600 PTAB←FIRSTPROP ATOM;
02700 LOOP: IF LASTPROP PTAB THEN RETURN NIL;
02800 TEM←SEEKPROP(PROPNAM PTAB,PROP);
02900 IF ¬NULL TEM THEN RETURN TEM;
03000 PTAB←NEXTPROP PTAB;
03100 GO LOOP;
03200 END;
03300
03400 EXPR INITPROP(IDENT,VALUE,NAME); RPLACD(IDENT,NAME.VALUE.CDR IDENT);
03600
03700 EXPR SEEKPROP(IDENT,PROPNAM);
03800 BEGIN SCALAR TEM;
03900 TEM←GETL(IDENT,LIST PROPNAM);
04000 IF NULL TEM THEN RETURN NIL;
04100 RETURN TEM;
04200 END;
04300
04400 %END%
04500
00100 %THIS SECTION DEFINES ALL COMMANDS IMPLEMENTING INFERENCE RULES%
00200
00300 FEXPR AE ARGS;
00400 BEGIN SCALAR WFF;
00500 WFF←WFFPART CAR ARGS;
00600 IF ¬(CAR WFF='AND) THEN ERREND '(FIRST ARG IS NOT AN AND);
00700 ADDLINE(ANDELIM1(WFF,CDR ARGS),'AE.ARGS,ASSPART CAR ARGS);
00800 END;
00900
01000 FEXPR AI ARGS;
01100 ADDLINE(CONJOIN WFFLIST ARGS,'AI.ARGS,UNION ASSLIST ARGS);
01200
01300 FEXPR ALT ARGS;
01400 BEGIN SCALAR NEWEXP;
01500 NEWEXP←ALT1(WFFPART CAR ARGS,WFFPART CADR ARGS);
01600 IF ¬VALID NEWEXP THEN ERREND '(LINES ARE NOT ALTERNATIVES);
01700 ADDLINE(NEWEXP,
01800 LIST('ALT.ARGS),
01900 UNION2(ASSPART CAR ARGS,ASSPART CADR ARGS));
02000 END;
02100
02200 FEXPR ASS PROP;
02300 ADDLINE(CAR PROP,'ASS.PROP,LIST NEXTLINE());
02400
02500 FEXPR BS ARGS;
02600 ADDLINE(BOUNDSUBST(WFFPART CAR ARGS,MAKECONSES CDR ARGS,NIL),
02700 'BS.ARGS,
02800 ASSPART CAR ARGS);
02900
03000 FEXPR DED LINES;
03100 BEGIN IF NULL LINES THEN ERREND '(NOTHING TO CONCLUDE);
03200 ADDLINE(LIST('IMPLIES,CONJOIN WFFLIST CDR LINES,WFFPART CAR LINES),
03300 'DED.LINES,
03400 SETDIF(ASSPART CAR LINES,CDR LINES));
03500 END;
03600
03700 FEXPR DEF ARGS;
03800 BEGIN IF ¬ATOM CAR ARGS THEN ERREND '(NAMES MUST BE ATOMS);
03900 ADDLINE('SETQ.ARGS,'DEF.ARGS,LIST NEXTLINE());
04000 END;
04100
04200 FEXPR DNE LINE;
04300 BEGIN SCALAR NEWSTAT;
04400 IF ¬VALID(NEWSTAT←DOUBLENEG WFFPART CAR LINE)
04500 THEN ERREND '(NO DOUBLE NEGATIVE);
04600 ADDLINE(NEWSTAT,'DNE.LINE,ASSPART CAR LINE);
04700 END;
04800
00100 FEXPR DNI LINE;
00200 ADDLINE(LIST('NOT,LIST('NOT,WFFPART CAR LINE)),
00300 'DNI.LINE,
00400 ASSPART CAR LINE);
00500
00600 FEXPR EG ARGS;
00700 ADDLINE(EXGEN1(WFFPART CAR ARGS,CDR ARGS),'EG.ARGS,ASSPART CAR ARGS);
00800
00900 FEXPR ELIM ARGS;
01000 BEGIN SCALAR NEW;
01100 NEW←WFFPART CADR ARGS;
01200 IF ¬((CAR NEW)='SETQ) THEN ERREND '(NO DEFINITION);
01300 ADDLINE(SUBST(CADDR NEW,CADR NEW,WFFPART CAR ARGS),
01400 'ELIM.ARGS,
01500 SETDIF(ASSPART CAR ARGS,ASSPART CADR ARGS));
01600 END;
01700
01800 FEXPR EQE ARGS;
01900 BEGIN SCALAR NEW;
02000 NEW←WFFPART CAR ARGS;
02100 IF ¬(CAR NEW='EQUIVALENT) THEN ERREND '(NO EQUIVALENCE);
02200 NEW←IF CADR ARGS=2 THEN REVERSE CDR NEW ELSE CDR NEW;
02300 ADDLINE('IMPLIES.NEW,'EQE.ARGS,ASSPART CAR ARGS);
02400 END;
02500
02600 FEXPR EQI ARGS;
02700 BEGIN SCALAR NEW;
02800 IF ¬VALID(NEW←EQI1(WFFPART CAR ARGS,WFFPART CAR ARGS))
02900 THEN ERREND '(ARE NOT EQUIVALENT);
03000 ADDLINE(NEW,'EQI.ARGS,UNION2(ASSPART CAR ARGS,ASSPART CADR ARGS));
03100 END;
03200
00100 FEXPR ES ARGS;
00200 ADDLINE(SPECALL(WFFPART CAR ARGS,CDR ARGS),
00300 'ES.ARGS,
00400 ASSPART CAR ARGS);
00500
00600 FEXPR IFE ARGS;
00700 BEGIN SCALAR NEW;
00800 IF ¬VALID(NEW←IFE1(WFFPART CAR ARGS,WFFPART CADR ARGS)) THEN
00900 ERREND '(NO IF-THEN-ELSE EXPRESSION);
01000 ADDLINE(NEW,'IFE.ARGS,UNION2(ASSPART CAR ARGS,ASSPART CADR ARGS));
01100 END;
01200
01300 FEXPR IFI ARGS;
01400 BEGIN SCALAR NEW;
01500 IF ¬VALID(NEW←IFI1(WFFPART CAR ARGS,WFFPART CADR ARGS)) THEN
01600 ERREND '(NEED IMPLICATIONS WITH OPPOSITE ANTECEDENTS);
01700 ADDLINE(NEW,'IFI.ARGS,UNION2(ASSPART CAR ARGS,ASSPART CADR ARGS));
01800 END;
01900
02000 FEXPR LC ARGS;
02100 ADDLINE(LIST('EQUAL,ARGS,LAMEXP ARGS),
02200 'LC.ARGS,
02300 NIL);
02400
02500 FEXPR MP ARGS;
02600 BEGIN SCALAR NEWSTAT;
02700 IF ¬ VALID(NEWSTAT←MP1(WFFPART CAR ARGS,WFFPART CADR ARGS))
02800 THEN ERREND '(CANNOT MODUS PONENS);
02900 ADDLINE(NEWSTAT,
03000 'MP.ARGS,
03100 UNION2(ASSPART CAR ARGS,ASSPART CADR ARGS));
03200 END;
03300
00100 FEXPR NE ARGS;
00200 BEGIN IF ¬VALID NOTELIM(WFFPART CAR ARGS,WFFPART CADR ARGS) THEN
00300 ERREND '(NO CONTRADICTION);
00400 ADDLINE('FALSE,
00500 'NE.ARGS,
00600 UNION2(ASSPART CAR ARGS,ASSPART CADR ARGS));
00700 END;
00800
00900 FEXPR NI IM;
01000 BEGIN SCALAR NEWSTAT;
01100 IF ¬VALID (NEWSTAT←NOTINTRO(WFFPART CAR IM)) THEN
01200 ERREND '(NO IMPLIES FALSE);
01300 ADDLINE(NEWSTAT,'NI.IM,ASSPART CAR IM);
01400 END;
01500
01600 FEXPR OE ARGS;
01700 BEGIN IF NULL ARGS∨NULL CDR ARGS THEN ERREND '(NEED AT LEAST TWO ARGS);
01800 ADDLINE(ORELIM1(WFFPART CAR ARGS,WFFLIST CDR ARGS),
01900 'OE.ARGS,
02000 UNION ASSLIST ARGS);
02100 END;
02200
02300 FEXPR OI ARGS;
02400 BEGIN SCALAR KNOWN,SAVARGS,WFFS;
02500 SAVARGS←ARGS;
02600 LOOP:IF NULL ARGS THEN IF NULL KNOWN THEN ERREND '(NO VALID PROPOSITION)
02700 ELSE GO ADDL;
02800 IF NUMBERP CAR ARGS THEN IF NULL KNOWN THEN KNOWN←CAR ARGS;
02900 IF NUMBERP CAR ARGS THEN WFFS←WFFPART CAR ARGS.WFFS
03000 ELSE WFFS←CAR ARGS.WFFS;
03100 ARGS←CDR ARGS;
03200 GO LOOP;
03300 ADDL: ADDLINE(IF NULL CDR WFFS THEN CAR WFFS ELSE 'OR.REVERSE WFFS,
03400 'OI.SAVARGS,
03500 ASSPART KNOWN);
03600 END;
03700
00100 FEXPR REP ARGS;
00200 BEGIN SCALAR NEW;
00300 NEW←WFFPART CADR ARGS;
00400 IF ¬ISEQUIVALENCE CAR NEW THEN ERREND '(NO EQUATION);
00500 NEW←IF CADDR ARGS=2 THEN REVERSE CDR NEW ELSE CDR NEW;
00600 ADDLINE(SUBST(CADR NEW,CAR NEW,WFFPART CAR ARGS),
00700 'REP.ARGS,
00800 UNION2(ASSPART CAR ARGS,ASSPART CADR ARGS));
00900 END;
01000
01100 FEXPR REPL ARGS;
01200 ADDLINE(REPEITHER(WFFPART CAR ARGS,WFFPART CADR ARGS,T,CADDR ARGS),
01300 'REPL.ARGS,
01400 UNION2(ASSPART CAR ARGS,ASSPART CADR ARGS));
01500
01600 FEXPR REPR ARGS;
01700 ADDLINE(REPEITHER(WFFPART CAR ARGS,WFFPART CADR ARGS,NIL,CADDR ARGS),
01800 'REPR.ARGS,
01900 UNION2(ASSPART CAR ARGS,ASSPART CADR ARGS));
02000
02100 FEXPR TAUT L;
02200 BEGIN IF ¬TH1(NIL,NIL,WFFLIST CDR L,LIST(CAR L)) THEN
02300 ERREND '(DOES NOT FOLLOW);
02400 ADDLINE(CAR L,'TAUT.L,UNION ASSLIST CDR L);
02500 END;
02600
02700 FEXPR UG ARGS;
02800 BEGIN SCALAR ASS,VARS,WFF;
02900 WFF←WFFPART CAR ARGS;
03000 ASS←ASSPART CAR ARGS;
03100 VARS←CDR ARGS;
03200 LOOP: IF NULL VARS THEN GO ADDL;
03300 IF ATOM CAR VARS THEN GO ATOM;
03400 IF CAAR VARS = 'CONS THEN GO DOT;
03500 ERREND '(ILLEGAL ARGUMENT);
03600 ATOM: WFF←UNGEN(WFF,ASS,CAR VARS,CAR VARS);
03700 GO ELOOP;
03800 DOT: WFF←UNGEN(WFF,ASS,CADAR VARS,CADDAR VARS);
03900 ELOOP:VARS←CDR VARS;
04000 GO LOOP;
04100 ADDL: ADDLINE(WFF,'UG.ARGS,ASSPART CAR ARGS);
04200 END;
04300
00100 FEXPR US ARGS;
00200 BEGIN ADDLINE(SPECALL(WFFPART CAR ARGS,CDR ARGS),
00300 'US.ARGS,
00400 ASSPART CAR ARGS);
00500 END;
00600
00700 FEXPR USEAX ARGS;
00800 BEGIN SCALAR AX,FORM;
00900 AX←GET(CAR ARGS,'AXIOM);
01000 IF NULL AX THEN ERREND '(NO SUCH AXIOM);
01100 FORM←SPECALL(AX,CDR ARGS);
01200 ADDLINE(FORM,'USEAX.ARGS,NIL);
01300 END;
01400
01500 FEXPR USESCHM ARGS;
01600 BEGIN SCALAR SCHEMA;
01700 SCHEMA←GET(CAR ARGS,'SCHEMA);
01800 IF NULL SCHEMA THEN ERREND '(IS NOT SCHEMA);
01900 ADDLINE(LAMEXP PROPSUBST(CADR ARGS,
02000 CADAR SCHEMA,
02100 CADR SCHEMA),
02400 'USESCHM.ARGS,
02500 NIL);
02600 END;
02700
02800 FEXPR USETHM ARGS;
02900 BEGIN SCALAR TH,FORM;
03000 TH←GET(CAR ARGS,'THEOREM);
03100 IF NULL TH THEN ERREND '(NO SUCH THEOREM);
03200 FORM←SPECALL(TH,CDR ARGS);
03300 ADDLINE(FORM,'USETHM.ARGS,NIL);
03400 END;
03500
03600 %END OF INFERENCE RULES%
03700
00100 %OTHER COMMANDS%
00200
00300 FEXPR BT LINO;
00400 BEGIN SCALAR PROOF;
00500 LINO←IF NULL LINO THEN CURLINE()-1 ELSE CAR LINO;
00600 PROOF←CURTEXT();
00700 IF LINO>CURLINE()∨LINO<0 THEN ERREND '(NON EXISTANT LINE);
00800 IF LINO=0 THEN PUTPROP(CURPROOF(),NIL,'PROOF) ELSE
00900 BEGIN RPLACD(NTHCDR(PROOF,LINO-1),NIL);
01000 PUTPROP(CURPROOF(),PROOF,'PROOF); END;
01100 INITPROOF CURPROOF();
01200 SHOWCURLINE();
01300 END;
01400
01500 FEXPR FINDL L;
01600 BEGIN SCALAR PRF,TXT,WFF;
01700 WFF←CAR L;
01800 PRF←IF ¬NULL CDR L THEN CADR L ELSE CURPROOF();
01900 TXT←GET(PRF,'PROOF);
02000 LOOP: IF NULL TXT THEN RETURN;
02100 IF WFF=CADAR TXT THEN SHOWLINE CAR TXT;
02200 TXT←CDR TXT;
02300 GO LOOP;
02400 END;
02500
02600 FEXPR GIVEAX L;
02700 BEGIN IF¬ATOM CAR L THEN ERREND '(NON ATOMIC AXIOM NAME);
02800 IF¬(CAR LεAXIOMS)THEN AXIOMS←APPEND(AXIOMS,LIST(CAR L));
02900 PUTPROP(CAR L,CADR L,'AXIOM);
03000 IF !*PRINT THEN SHOWAXIOM CAR L;
03100 END;
03200
03300 FEXPR GIVESCHM L;
03400 BEGIN IF¬(ATOM CAR L) THEN ERREND '(NON ATOMIC SCHEMA NAME);
03500 IF¬(MEMBER(CAR L,SCHEMAS))THEN SCHEMAS←APPEND(SCHEMAS,LIST(CAR L));
03600 PUTPROP(CAR L,CADR L,'SCHEMA);
03700 IF !*PRINT THEN SHOWSCHEMA CAR L;
03800 END;
03900
04000 EXPR INVENTORY;
04100 BEGIN IF ¬(NULL AXIOMS) THEN
04200 BEGIN TERPRI(); PRINT 'AXIOMS: ; PRINL AXIOMS; END;
04300 IF ¬(NULL SCHEMAS) THEN
04400 BEGIN TERPRI(); PRINT 'SCHEMAS: ; PRINL SCHEMAS; END;
04500 IF ¬(NULL PROOFS) THEN
04600 BEGIN TERPRI(); PRINT 'PROOFS: ; PRINL PROOFS; END;
04700 IF ¬(NULL THEOREMS) THEN
04800 BEGIN TERPRI(); PRINT 'THEOREMS: ; PRINL THEOREMS; END;
04900 END;
05000
00100 FEXPR MAKETHM ARG;
00200 MAKETHEOREM1(CAR ARG,
00300 CADR ARG,
00400 IF ¬(NULL CDDR ARG) THEN CADDR ARG ELSE CURPROOF());
00500
00600 EXPR ONDD;
00700 BEGIN INITSTANCHARSET(); LINELENGTH(CONSOLEWIDTH←DDWIDTH); END;
00800
00900 EXPR ONIII;
01000 BEGIN INITSTANCHARSET(); LINELENGTH(CONSOLEWIDTH←IIIWIDTH); END;
01100
01200 EXPR ONIMLAC;
01300 BEGIN INITSTANCHARSET(); LINELENGTH(CONSOLEWIDTH←IMLACWIDTH); END;
01400
01500 EXPR ONTTY;
01600 BEGIN INITTTYCHARSET(); LINELENGTH(CONSOLEWIDTH←TTYWIDTH); END;
01700
01800 FEXPR PROOF NAME;
01900 BEGIN IF NULL NAME THEN ERREND '(NO NAME GIVEN);
02000 IF ¬ATOM CAR NAME THEN ERREND '(NON ATOMIC PROOF NAME);
02100 INITPROOF CAR NAME;
02200 IF !*PRINT THEN SHOWCURLINE();
02300 END;
02400
02500 FEXPR REDO ARGS;
02600 BEGIN SCALAR CHANGED,CURL,LASTL,NEWC;
02700 IF ¬EQUAL(WFFPART CAR ARGS,WFFPART CADR ARGS) THEN
02800 ERREND '(CANNOT REDO);
02900 CHANGED←(CAR ARGS.CADR ARGS).NIL;
03000 CURL←CAR ARGS+1;
03100 LASTL←CURLINE()+1;
03200 LOOP: IF CURL EQ LASTL THEN RETURN NIL;
03300 NEWC←SUBLIS(CHANGED,BYPART CURL);
03400 IF NEWC EQUAL BYPART CURL THEN GO ELOOP ELSE
03500 EVAL NEWC;
03600 CHANGED←(CURL.CURLINE()).CHANGED;
03700 ELOOP: CURL←CURL+1;
03800 GO LOOP;
03900 END;
04000
00100 FEXPR RESTOREALL FILES;
00200 BEGIN SCALAR DEV,FILE,!*PRINT;
00300 IF !*FILEPRINT THEN ON PRINT;
00400 DEV←'DSK: ;
00500 LOOP: IF NULL FILES THEN GO EXIT;
00600 FILE←CAR FILES;
00700 IF ATOM FILE THEN GO READ;
00800 IF CAR FILE='QUOTE THEN GO DEVICE;
00900 IF CAR FILE='CONS THEN GO DOTTED;
01000 ERREND '(NOT FILE OR DEVICE NAME);
01100 READ: READIN(DEV,LIST FILE,NIL);
01200 GO ELOOP;
01300 DOTTED:FILE←CADR FILE.CADDR FILE;
01400 GO READ;
01500 DEVICE:DEV←CADR FILE;
01600 GO ELOOP;
01700 ELOOP: FILES←CDR FILES;
01800 GO LOOP;
01900 EXIT: INVENTORY();
02000 END;
02100
02200 FEXPR SAVEALL FILE;
02300 BEGIN SCALAR DEV,ITEM;
02400 DEV←'DSK: ;
02500 LOOP: IF NULL FILE THEN ERREND '(DEVICE BUT NO FILE);
02600 ITEM←CAR FILE;
02700 IF ATOM ITEM THEN GO OUTPUT;
02800 IF CAR ITEM='QUOTE THEN GO DEVICE;
02900 IF CAR ITEM='CONS THEN GO DOTTED;
03000 ERREND '(NOT FILE SPECIFIER);
03100 DEVICE:DEV←CADR ITEM;
03200 FILE←CDR FILE;
03300 GO LOOP;
03400 DOTTED:ITEM←CADR ITEM.CADDR ITEM;
03500 OUTPUT:EVAL LIST('OUTPUT,DEV,ITEM);
03600 OUTC(T,NIL);
03700 LINELENGTH FILEWIDTH;
03800 MAPC(FUNCTION SAVEAXIOM,AXIOMS);
03900 MAPC(FUNCTION SAVESCHEMA,SCHEMAS);
04000 MAPC(FUNCTION SAVEPROOF,PROOFS);
04100 MAPC(FUNCTION SAVETHEOREM,THEOREMS);
04200 OUTC(NIL,T);
04300 INVENTORY();
04400 END;
04500
00100 FEXPR SAVECOMS FILE;
00200 BEGIN SCALAR DEV,ITEM;
00300 DEV←'DSK: ;
00400 LOOP: IF NULL FILE THEN ERREND '(NO FILE SPECIFIED);
00500 ITEM←CAR FILE;
00600 IF ATOM ITEM THEN GO OUTPUT;
00700 IF CAR ITEM='QUOTE THEN GO DEVICE;
00800 IF CAR ITEM='CONS THEN GO DOTTED;
00900 ERREND '(NOT FILE SPECIFIER);
01000 DEVICE:DEV←CADR ITEM;
01100 FILE←CDR FILE;
01200 GO LOOP;
01300 DOTTED:ITEM←CADR ITEM.CADDR ITEM;
01400 OUTPUT:EVAL LIST('OUTPUT,DEV,ITEM);
01500 OUTC(T,NIL);
01600 LINELENGTH FILEWIDTH;
01700 MAPC(FUNCTION SAVEAXCOM,AXIOMS);
01800 MAPC(FUNCTION SAVESCHMCOM,SCHEMAS);
01900 MAPC(FUNCTION SAVEPRFCOM,PROOFS);
02000 MAPC(FUNCTION SAVETHMCOM,THEOREMS);
02100 OUTC(NIL,T);
02200 INVENTORY();
02300 END;
02400
02500 FEXPR SHOW THINGS;
02600 BEGIN SCALAR LINE1,LINE2,TEM;
02700 TOP: IF NULL THINGS THEN RETURN SHOWPROOF CURPROOF();
02800 LOOP: IF NULL THINGS THEN GO EXIT;
02900 IF ¬ATOM CAR THINGS THEN GO DEV;
03000 IF NUMBERP CAR THINGS THEN GO LINES;
03100 TEM←GETGET(CAR THINGS,'IMAGE);
03200 IF NULL TEM THEN ERREND '(NOTHING TO SHOW);
03300 % (CADR TEM)(CAR THINGS);
03350 EVAL '((CADR TEM) (CAR THINGS)); %TONY BUG PATCH
03400 ELOOP:THINGS←CDR THINGS;
03500 GO LOOP;
03600 LINES:LINE1←CAR THINGS; THINGS←CDR THINGS;
03700 IF NULL THINGS∨¬NUMBERP CAR THINGS THEN LINE2←LINE1 ELSE
03800 BEGIN LINE2←CAR THINGS; THINGS←CDR THINGS; END;
03900 LLOOP:IF LINE1>LINE2 THEN GO EXIT;
04000 SHOWLINE GETLINE LINE1;
04100 LINE1←LINE1+1;
04200 GO LLOOP;
04300 DEV: IF ¬(CAAR THINGS='QUOTE) THEN ERREND '(NEED NAME OR FILE SPEC);
04400 EVAL('OUTPUT.CADAR THINGS);
04500 OUTC(T,T);
04600 THINGS←CDR THINGS;
04700 GO TOP;
04800 EXIT: OUTC(NIL,T);
04900 END;
05000
00100 FEXPR SHOWALL FILE;
00200 BEGIN SCALAR DEV,ITEM;
00300 DEV←'DSK: ;
00400 LOOP: IF NULL FILE THEN ERREND '(NO FILE SPECIFIED);
00500 ITEM←CAR FILE;
00600 IF ATOM ITEM THEN GO OUTPUT;
00700 IF CAR ITEM='QUOTE THEN GO DEVICE;
00800 IF CAR ITEM='CONS THEN GO DOTTED;
00900 ERREND '(NOT FILE SPECIFIER);
01000 DEVICE:DEV←CADR ITEM;
01100 FILE←CDR FILE;
01200 GO LOOP;
01300 DOTTED:ITEM←CADR ITEM.CADDR ITEM;
01400 OUTPUT:EVAL LIST('OUTPUT,DEV,ITEM);
01500 OUTC(T,NIL);
01600 LINELENGTH FILEWIDTH;
01700 MAPC(FUNCTION SHOWAXIOM,AXIOMS);
01800 MAPC(FUNCTION SHOWSCHEMA,SCHEMAS);
01900 MAPC(FUNCTION SHOWPROOF,PROOFS);
02000 MAPC(FUNCTION SHOWTHEOREM,THEOREMS);
02100 OUTC(NIL,T);
02200 INVENTORY();
02300 END;
02400
02500 FEXPR SSEX L;
02600 BEGIN SCALAR LINE,NAME,PRF;
02700 NAME←IF NULL L THEN CURPROOF() ELSE CAR L;
02800 PRF←GETL(NAME,'(PROOF));
02900 IF NULL PRF THEN ERREND '(NO PROOF BY THAT NAME);
03000 PRF←CADR PRF;
03100 PRINT 'PROOF ; PRINS NAME;
03200 LOOP: IF NULL PRF THEN RETURN;
03300 LINE←CAR PRF;
03400 TERPRI();
03500 PRINC CAR LINE; PRINC '/ ;
03600 PRINTSUBEXPR(CADR LINE,CURCOL(),0);
03700 IF FLATSIZE CDDR LINE+6>CHRCT() THEN GO MANY;
03800 PRINC '/ ; PRINS 'BY ; PRINS CADDR LINE;
03900 IF ¬NULL CADDDR LINE THEN
04000 BEGIN PRINS 'ASS ; PRIN1 CADDDR LINE; END;
04100 ELOOP: PRF←CDR PRF;
04200 GO LOOP;
04300 MANY: TERPRI(); PRINTN('/ ,4); PRINC ' BY ;
04400 PRINC '/ ; PRINTSUBEXPR(CADDR LINE,CURCOL(),0);
04500 IF NULL CADDDR LINE THEN GO ELOOP;
04600 TERPRI(); PRINTN('/ ,4); PRINC ' ASS ;
04700 PRINC '/ ; PRINS CADDDR LINE;
04800 GO ELOOP;
04900 END;
05000
05100 %END%
05200
00100 EXPR ADDLINE(WFF,JUST,ASS);
00200 BEGIN PUTPROP(CURPROOF(),
00300 NCONC(CURTEXT(),LIST LIST(CURLINE()+1,WFF,JUST,ASS)),
00400 'PROOF);
00500 CURLIN←CURLIN+1;
00600 PUTPROP('!@,CURLINE(),'NEWNAM);
00700 IF !*PRINT THEN SHOWCURLINE();
00800 END;
00900
01000 FEXPR ADDAXIOM L;
01100 BEGIN PUTPROP(CAR L,CADR L,'AXIOM); AXIOMS←CAR L.AXIOMS; END;
01200
01300 FEXPR ADDSCHEMA L; BEGIN PUTPROP(CAR L,CADR L,'SCHEMA);
01400 SCHEMAS←CAR L.SCHEMAS;
01500 END;
01600
01700 FEXPR ADDTHEOREM L;
01800 BEGIN PUTPROP(CAR L,CADR L,'THEOREM);
01900 THEOREMS←CAR L.THEOREMS;
02000 END;
02100
02200 EXPR ALPHAPART IDENT;
02300 BEGIN SCALAR CHARS;
02400 CHARS←REVERSE EXPLODE IDENT;
02500 LOOP: IF ¬NUMBERP CAR CHARS THEN RETURN READLIST REVERSE CHARS;
02600 CHARS←CDR CHARS;
02700 GO LOOP;
02800 END;
02900
03000 EXPR ALLVARS EXPRESSION; ALLVARS1(EXPRESSION,NIL);
03100
03200 EXPR ALLVARS1(EXP,VARS);
03300 IF ATOM EXP
03400 THEN IF ISVAR EXP
03500 THEN IF EXPεVARS THEN VARS ELSE EXP.VARS ELSE VARS
03600 ELSE ALLVARSL(CDR EXP,VARS);
03700
03800 EXPR ALLVARSL(EXPL,VARS);
03900 IF NULL EXPL THEN VARS ELSE ALLVARS1(CAR EXPL,ALLVARSL(CDR EXPL,VARS));
04000
00100 EXPR ALT1(I1,I2);
00200 (LAMBDA (U,V);IF VALID U THEN SUBLIS(U,'QQQ) ELSE
00300 IF VALID V THEN SUBLIS(V,'QQQ) ELSE
00400 'INVALID)
00500 (INST(I1.I2,'((IMPLIES PPP QQQ) IMPLIES (NOT PPP) QQQ),NIL),
00600 INST(I2.I1,'((IMPLIES PPP QQQ) IMPLIES (NOT PPP) QQQ),NIL));
00700
00800 EXPR ANDELIM1(WFF,PLACES);
00900 BEGIN SCALAR CHOSEN,LEN;
01000 LEN←LENGTH CDR WFF;
01100 IF CAR WFF≠'AND THEN ERREND '(FIRST ARG IS NOT AN AND);
01200 LOOP: IF NULL PLACES THEN RETURN CONJOIN REVERSE CHOSEN;
01300 IF CAR PLACES>LEN THEN ERREND '(TOO FEW CONJUNCTS);
01400 CHOSEN←NTHELT(CDR WFF,CAR PLACES).CHOSEN;
01500 PLACES←CDR PLACES;
01600 GO LOOP;
01700 END;
01800
01900 EXPR ASSLIST L; MAPCAR(FUNCTION ASSPART,L);
02000
02100 EXPR ASSOCR(ITM,LST);
02200 BEGIN
02300 LOOP: IF NULL LST THEN RETURN;
02400 IF ITM EQ CDAR LST THEN RETURN CAR LST;
02500 LST←CDR LST;
02600 GO LOOP;
02700 END;
02800
02900 EXPR ASSPART LINE; CADDDR GETLINE LINE;
03000
03100 EXPR BINAND ARGS;
03200 IF NULL ARGS THEN '(AND TRUE TRUE) ELSE
03300 IF NULL CDR ARGS THEN LIST('AND,CAR ARGS,'TRUE) ELSE
03400 IF NULL CDDR ARGS THEN 'AND.ARGS ELSE
03500 LIST('AND,CAR ARGS,BINAND CDR ARGS);
03600
03700 EXPR BINOR ARGS;
03800 IF NULL ARGS THEN '(OR FALSE FALSE) ELSE
03900 IF NULL CDR ARGS THEN LIST('OR,CAR ARGS,'FALSE) ELSE
04000 IF NULL CDDR ARGS THEN 'OR.ARGS ELSE
04100 LIST('OR,CAR ARGS,BINOR CDR ARGS);
04200
04300 EXPR BYPART LINE; CADDR GETLINE LINE;
04400
00100 EXPR BOUNDSUBST(EXP,SUBS,BINDS);
00200 BEGIN SCALAR TEM;
00300 IF ATOM EXP THEN GO ATOM;
00400 IF ISQUANT CAAR EXP THEN GO QUANT;
00500 RETURN BOUNDSUBSTL(EXP,SUBS,BINDS);
00600 ATOM: IF ISCONST EXP THEN RETURN EXP;
00700 TEM←ASSOC(EXP,BINDS);
00800 IF ¬NULL TEM THEN RETURN CDR TEM;
00900 TEM←ASSOCR(EXP,BINDS);
01000 IF ¬NULL TEM THEN ERREND '(FREE VARIABLE CAPTURE);
01100 RETURN EXP;
01200 QUANT:TEM←ASSOC(CADAR EXP,SUBS);
01300 TEM←IF ¬NULL TEM THEN CDR TEM ELSE CADAR EXP;
01400 IF ¬NULL ASSOCR(TEM,BINDS) THEN ERREND '(BOUND VARIABLE CAPTURE);
01500 RETURN LIST(LIST(CAAR EXP,TEM),
01600 BOUNDSUBST(CADR EXP,SUBS,(CADAR EXP.TEM).BINDS));
01700 END;
01800
01900 EXPR BOUNDSUBSTL(LST,SUBS,BINDS);
02000 IF NULL LST
02100 THEN NIL
02200 ELSE BOUNDSUBST(CAR LST,SUBS,BINDS).BOUNDSUBSTL(CDR LST,SUBS,BINDS);
02300
02400 EXPR CONJOIN WFFS; IF NULL WFFS THEN 'TRUE ELSE
02500 IF NULL CDR WFFS THEN CAR WFFS ELSE
02600 'AND.WFFS;
02700
02800 EXPR CURCOL; LINELENGTH NIL+1-CHRCT();
02900
03000 EXPR CURLINE; PROG2(CURPROOF(),CURLIN);
03100
03200 EXPR CURPROOF; IF NULL CURPRF THEN ERREND '(NO CURRENT PROOF) ELSE CURPRF;
03300
03400 EXPR CURTEXT; GET(CURPROOF(),'PROOF);
03500
03600 EXPR DOUBLENEG(PROP);
03700 (LAMBDA(W);IF ¬VALID W THEN 'INVALID ELSE SUBLIS(W,'PPP))
03800 INST(PROP,'(NOT (NOT PPP)),NIL);
03900
04000 EXPR EXGEN1(WFF,VARS);
04100 BEGIN
04200 LOOP: IF NULL VARS THEN RETURN WFF;
04300 IF ATOM CAR VARS THEN GO ATOM;
04400 IF CAAR VARS = 'CONS THEN GO DOT;
04500 ERREND '(ILLEGAL ARGUMENT);
04600 ATOM: WFF←EXGEN(WFF,CAR VARS,CAR VARS);
04700 GO ELOOP;
04800 DOT: WFF←EXGEN(WFF,CADAR VARS,CADDAR VARS);
04900 ELOOP:VARS←CDR VARS;
05000 GO LOOP;
05100 END;
05200
00100 EXPR EXGEN(WFF,OLD,NEW);
00200 BEGIN SCALAR TEM,WFF;
00300 TEM←GENSYM();
00400 WFF←SUBST(TEM,OLD,WFF);
00500 IF NEWεALLVARS WFF THEN ERREND '(NEW VARIABLE CONFLICTS);
00600 RETURN LIST(LIST('THEREEXISTS,NEW),SUBST(NEW,TEM,WFF));
00700 END;
00800
00900 EXPR EQI1(WFF1,WFF2);
01000 (LAMBDA W;IF ¬VALID W THEN 'INVALID
01100 ELSE SUBLIS(W,'(EQUIVALENT PPP QQQ)))
01200 INST(WFF1.WFF2,'((IMPLIES PPP QQQ) IMPLIES QQQ PPP),NIL);
01300
01400 EXPR ERREND MESSAGE; BEGIN PRINT MESSAGE; ERR(); END;
01500
01600 EXPR FREEIN(VAR,LINES);
01700 IF NULL LINES THEN NIL ELSE
01800 IF MEMBER(VAR,FREEVARS WFFPART CAR LINES) THEN T ELSE
01900 FREEIN(VAR,CDR LINES);
02000
02100 EXPR FREEVARS(EXPRESSION); FREEVARS1(NIL,NIL,EXPRESSION);
02200
02300 EXPR FREEVARS1(BVARS,FVARS,EXP);
02400 IF ATOM EXP THEN IF ISVAR EXP THEN
02500 IF MEMBER(EXP,BVARS) THEN FVARS ELSE
02600 IF MEMBER(EXP,FVARS) THEN FVARS ELSE
02700 EXP.FVARS ELSE FVARS ELSE
02800 IF ATOM CAR EXP THEN FREEVARS2(BVARS,FVARS,CDR EXP) ELSE
02900 IF ATOM CAAR EXP THEN
03000 (IF MEMBER(CAAR EXP,'(FORALL THEREEXISTS)) THEN
03100 FREEVARS1(CADAR EXP.BVARS,FVARS,CADDR EXP))
03200 ELSE ERREND '(UNKNOWN NONATOMIC FUNCTION);
03300
03400 EXPR FREEVARS2(BVARS,FVARS,EXPL);
03500 IF NULL EXPL THEN FVARS ELSE
03600 FREEVARS1(BVARS,FREEVARS2(BVARS,FVARS,CDR EXPL),CAR EXPL);
03700
00100 EXPR GETCURLINE; GETLINE CURLINE();
00200
00300 EXPR GETLINE LINENO;
00400 BEGIN SCALAR TEM;
00500 TEM←ASSOC(LINENO,CURTEXT());
00600 IF NULL TEM THEN ERREND '(NO SUCH LINE);
00700 RETURN TEM;
00800 END;
00900
01000 FEXPR GIVEPROOF L;
01100 BEGIN IF¬ATOM CAR L THEN ERREND '(NON ATOMIC PROOF NAME);
01200 IF¬(CAR LεPROOFS)THEN PROOFS←APPEND(PROOFS,LIST(CAR L));
01300 PUTPROP(CAR L,CADR L,'PROOF);
01400 END;
01500
01600 EXPR IFE1(WFF1,WFF2);
01700 (LAMBDA(W,X,Y,Z);
01800 IF VALID W THEN SUBLIS(W,'QQQ) ELSE
01900 IF VALID X THEN SUBLIS(X,'RRR) ELSE
02000 IF VALID Y THEN SUBLIS(Y,'QQQ) ELSE
02100 IF VALID Z THEN SUBLIS(Z,'RRR) ELSE 'INVALID)
02200 (INST(WFF1.WFF2,'(PPP COND (PPP QQQ) (T RRR)),NIL),
02300 INST(WFF1.WFF2,'((NOT PPP) COND (PPP QQQ) (T RRR)),NIL),
02400 INST(WFF2.WFF1,'(PPP COND (PPP QQQ) (T RRR)),NIL),
02500 INST(WFF2.WFF1,'((NOT PPP) COND (PPP QQQ) (T RRR)),NIL));
02600
02700 EXPR IFI1(WFF1,WFF2);
02800 (LAMBDA(W,X);
02900 IF VALID W THEN SUBLIS(W,'(COND (PPP QQQ) (T RRR))) ELSE
03000 IF VALID X THEN SUBLIS(X,'(COND (PPP QQQ) (T RRR))) ELSE 'INVALID)
03100 (INST(WFF1.WFF2,'((IMPLIES PPP QQQ) IMPLIES (NOT PPP) RRR),NIL),
03200 INST(WFF2.WFF1,'((IMPLIES PPP QQQ) IMPLIES (NOT PPP) RRR),NIL));
03300
00100 EXPR INITALL;
00200 BEGIN CURPRF←NIL;
00300 AXIOMS←NIL;
00400 THEOREMS←NIL;
00500 PROOFS←NIL;
00600 SCHEMAS←NIL;
00700 END;
00800
00900 EXPR INITOPS;
01000 BEGIN SCALAR INCR,OP,PREC,PRECLIS;
01100 PRECLIS←'!*COMMA!*.'SETQ.PRECLIS!*;
01200 LOOP: IF NULL PRECLIS THEN RETURN;
01300 OP←CAR PRECLIS;
01400 PREC←GET(OP,'INFIX);
01500 INCR←IF GET(OP,'LEFT) THEN -1 ELSE 1;
01600 PUTPROP(OP,LIST(3*PREC+INCR,3*PREC-INCR),'PREC);
01700 PRECLIS←CDR PRECLIS;
01800 GO LOOP;
01900 END;
02000
02100 EXPR INITPROOF NAME;
02200 BEGIN IF NULL NAME THEN ERREND '(NIL NOT ACCEPTABLE PROOF NAME);
02300 CURPRF←NAME;
02400 IF GETL(NAME,'(PROOF)) THEN GO EXIST;
02500 PUTPROP(NAME,NIL,'PROOF);
02600 PROOFS←APPEND(PROOFS,LIST NAME);
02700 EXIST:CURLIN←IF NULL CURTEXT() THEN 0 ELSE CAAR LAST CURTEXT();
02800 PUTPROP('!@,CURLINE(),'NEWNAM);
02900 END;
03000
00100 EXPR INITSTANCHARSET;
00200 BEGIN PUTPROP('AND,'!∧,'INFXNAM);
00300 PUTPROP('CMAPS,'!→!→,'INFXNAM);
00400 PUTPROP('!*COMMA!*,'!,,'INFXNAM);
00500 PUTPROP('CONS,'!.,'INFXNAM);
00600 PUTPROP('CONTAINED,'!⊂,'INFXNAM);
00700 PUTPROP('DIFFERENCE,'!-,'INFXNAM);
00800 PUTPROP('EQUAL,'!=,'INFXNAM);
00900 PUTPROP('EQUIVALENT,'!≡,'INFXNAM);
01000 PUTPROP('EXPT,'!↑,'INFXNAM);
01100 PUTPROP('FORALL,'!∀,'INFXNAM);
01200 PUTPROP('GEQ,'!≥,'INFXNAM);
01300 PUTPROP('GREATERP,'!>,'INFXNAM);
01400 PUTPROP('IMPLIES,'!⊃,'INFXNAM);
01500 PUTPROP('INTERSECTION,'!∩,'INFXNAM);
01600 PUTPROP('LAMBDA,'!λ,'INFXNAM);
01700 PUTPROP('LEQ,'!≤,'INFXNAM);
01800 PUTPROP('LESSP,'!<,'INFXNAM);
01900 PUTPROP('MAPS,'!→,'INFXNAM);
02000 PUTPROP('MEMBER,'!ε,'INFXNAM);
02100 PUTPROP('MINUS,'!-,'INFXNAM);
02200 PUTPROP('NEQ,'!≠,'INFXNAM);
02300 PUTPROP('NOT,'!¬,'INFXNAM);
02400 PUTPROP('OR,'!∨,'INFXNAM);
02500 PUTPROP('PLUS,'!+,'INFXNAM);
02600 PUTPROP('PRODUCT,'!⊗,'INFXNAM);
02700 PUTPROP('QUOTE,'!','INFXNAM);
02800 PUTPROP('QUOTIENT,'!/,'INFXNAM);
02900 PUTPROP('SETQ,'!←,'INFXNAM);
03000 PUTPROP('THEREEXISTS,'!∃,'INFXNAM);
03100 PUTPROP('TIMES,'!*,'INFXNAM);
03200 PUTPROP('UNION,'!∪,'INFXNAM);
03300 END;
03400
00100 EXPR INITTTYCHARSET;
00200 BEGIN PUTPROP('AND,'!&,'INFXNAM);
00300 PUTPROP('CMAPS,'! CMAPS! ,'INFXNAM);
00400 PUTPROP('!*COMMA!*,'!,,'INFXNAM);
00500 PUTPROP('CONS,'!.,'INFXNAM);
00600 PUTPROP('CONTAINED,'! CONT! ,'INFXNAM);
00700 PUTPROP('DIFFERENCE,'!-,'INFXNAM);
00800 PUTPROP('EQUAL,'!=,'INFXNAM);
00900 PUTPROP('EQUIVALENT,'!<=>,'INFXNAM);
01000 PUTPROP('EXPT,'!↑,'INFXNAM);
01100 PUTPROP('FORALL,'!A,'INFXNAM);
01200 PUTPROP('GEQ,'!>!=,'INFXNAM);
01300 PUTPROP('GREATERP,'!>,'INFXNAM);
01400 PUTPROP('IMPLIES,'!=!>,'INFXNAM);
01500 PUTPROP('INTERSECTION,'! INTERSECT! ,'INFXNAM);
01600 PUTPROP('LAMBDA,'!L,'INFXNAM);
01700 PUTPROP('LEQ,'!<!=,'INFXNAM);
01800 PUTPROP('LESSP,'!<,'INFXNAM);
01900 PUTPROP('MAPS,'! MAPS! ,'INFXNAM);
02000 PUTPROP('MEMBER,'! MEMBER! ,'INFXNAM);
02100 PUTPROP('MINUS,'!-,'INFXNAM);
02200 PUTPROP('NEQ,'! NEQ! ,'INFXNAM);
02300 PUTPROP('NOT,'!-,'INFXNAM);
02400 PUTPROP('OR,'! V! ,'INFXNAM);
02500 PUTPROP('PLUS,'!+,'INFXNAM);
02600 PUTPROP('PRODUCT,'! PROD! ,'INFXNAM);
02700 PUTPROP('QUOTE,'!','INFXNAM);
02800 PUTPROP('QUOTIENT,'!/,'INFXNAM);
02900 PUTPROP('SETQ,'!←,'INFXNAM);
03000 PUTPROP('THEREEXISTS,'!E,'INFXNAM);
03100 PUTPROP('TIMES,'!*,'INFXNAM);
03200 PUTPROP('UNION,'! UNION! ,'INFXNAM);
03300 END;
03400
00100 EXPR INST(EXP,MODEL,PAIRS);
00200 IF ¬VALID PAIRS THEN 'INVALID ELSE
00300 IF ATOM MODEL THEN
00400 (IF MODELε'(PPP QQQ RRR SSS) THEN
00500 (LAMBDA(W); IF NULL W THEN (MODEL.EXP).PAIRS ELSE
00600 IF CDR W = EXP THEN PAIRS ELSE
00700 'INVALID)
00800 (ASSOC(MODEL,PAIRS)) ELSE
00900 IF MODEL EQ EXP THEN PAIRS ELSE
01000 'INVALID) ELSE
01100 IF ATOM EXP THEN 'INVALID ELSE
01200 INST(CDR EXP,CDR MODEL,INST(CAR EXP,CAR MODEL,PAIRS));
01300
01400 EXPR ISCONST X; NUMBERP X ∨ XεLOGICALCONSTANTS;
01500
01600 EXPR ISEQUIVALENCE WFF; WFFε'(EQUAL EQUIVALENT SETQ);
01700
01800 EXPR ISIDENT X; ATOM X ∧ ¬NUMBERP X;
01900
02000 EXPR ISQUANT X; XεQUANTIFIERS;
02100
02200 EXPR ISVAR X; ISIDENT X ∧ ¬ISCONST X;
02300
02400 EXPR LAMEXP FORMULA;
02500 IF ATOM FORMULA THEN FORMULA ELSE
02600 IF ATOM CAR FORMULA THEN CAR FORMULA.LAMEXPL CDR FORMULA ELSE
02700 IF CAAAR FORMULA='LAMBDA
02800 THEN PROPSUBST(CADR FORMULA,CADAAR FORMULA,CADAR FORMULA) ELSE
02900 LAMEXP CAR FORMULA.LAMEXPL CDR FORMULA;
03000
03100 EXPR LAMEXPL LIST; MAPCAR(FUNCTION LAMEXP,LIST);
03200
00100 EXPR MAKECONSES L;
00200 BEGIN SCALAR RES;
00300 LOOP: IF NULL L THEN RETURN RETURN RES;
00400 IF ATOM CAR L∨CAAR L≠'CONS ∨LENGTH CAR L≠3
00500 THEN ERREND '(BAD ARGUMENT);
00600 RES←(CADAR L.CADDAR L).RES;
00700 L←CDR L;
00800 GO LOOP;
00900 END;
01000
01100 EXPR MAKERNL(FREEV,ALLV);
01200 BEGIN SCALAR CNT,ID,NVAR,NEWVARS,VAR;
01300 LOOP: IF NULL FREEV THEN RETURN NEWVARS;
01400 VAR←CAR FREEV;
01500 IF VARεALLV THEN GO MAKE;
01600 ELOOP:FREEV←CDR FREEV;
01700 GO LOOP;
01800 MAKE: ID←ALPHAPART(VAR);
01900 CNT←1;
02000 MAKE1:NVAR←MAKESYM(ID,CNT);
02100 IF NVARεALLV THEN GO EMAKE;
02200 NEWVARS←(VAR.NVAR).NEWVARS;
02300 GO ELOOP;
02400 EMAKE:CNT←CNT+1;
02500 GO MAKE1;
02600 END;
02700
02800 EXPR MAKEVAR(V,L);
02900 BEGIN SCALAR TEM; TEM←MAKERNL(LIST V,L);
03000 RETURN IF NULL TEM THEN V ELSE CDAR TEM;
03100 END;
03200
03300 EXPR MAKESYM(IDENT,NUM); READLIST(APPEND(EXPLODE IDENT,EXPLODE NUM));
03400
03500 EXPR MAKETHEOREM1(THEOREM,LINE,PROOF);
03600 BEGIN INITPROOF PROOF;
03700 IF ¬NULL ASSPART LINE THEN
03800 ERREND '(STILL HAS ASSUMPTIONS);
03900 PUTPROP(THEOREM,WFFPART LINE,'THEOREM);
04000 PUTPROP(THEOREM,LIST(LINE,PROOF),'BY);
04100 THEOREMS←APPEND(THEOREMS,LIST(THEOREM));
04200 IF !*PRINT THEN SHOWTHEOREM THEOREM;
04300 END;
04400
04500 EXPR MP1(U,V);
04600 BEGIN SCALAR W;
04700 W←INST(U.V,'(PPP IMPLIES PPP QQQ),NIL);
04800 IF ¬VALID W THEN W←INST(V.U,'(PPP IMPLIES PPP QQQ),NIL);
04900 IF ¬VALID W THEN RETURN 'INVALID ELSE
05000 RETURN SUBLIS(W,'QQQ);
05100 END;
05200
00100 EXPR NEXTLINE; CURLINE()+1;
00200
00300 EXPR NOTELIM(X,NOTX);
00400 (LAMBDA (X,Y); IF ¬VALID X THEN Y ELSE X)
00500 (INST(X.NOTX,'(PPP NOT PPP),NIL),INST(NOTX.X,'(PPP NOT PPP),NIL));
00600
00700 EXPR NOTINTRO PROP;
00800 (LAMBDA W;IF ¬VALID W THEN 'INVALID ELSE SUBLIS(W,'(NOT PPP)))
00900 INST(PROP,'(IMPLIES PPP FALSE),NIL);
01000
01100 EXPR NTHCDR(L,N); IF N=0 THEN L ELSE NTHCDR(CDR L,N-1);
01200
01300 EXPR NTHELT(L,N); CAR NTHCDR(L,N-1);
01400
01500 EXPR NUMPART LINE; CAR GETLINE LINE;
01600
01700 EXPR ORELIM1(DISJUN,IMPS);
01800 BEGIN SCALAR ANTECEDS,PREMS,RES;
01900 IF CAR DISJUN≠'OR THEN ERREND '(FIRST ARG MUST BE DISJUNCTION);
02000 IF NULL CDR DISJUN THEN ERREND '(NO DISJUNCTS);
02100 IF NULL IMPS THEN ERREND '(NEED AT LEAST ONE IMPLICATION);
02200 PREMS←CDR DISJUN;
02300 RES←CDDAR IMPS;
02400 LOOP1:IF CAAR IMPS≠'IMPLIES THEN ERREND '(ARG NOT IMPLICATION);
02500 IF CDDAR IMPS≠RES THEN ERREND '(MULTIPLE CONCLUSIONS);
02600 ANTECEDS←CADAR IMPS.ANTECEDS;
02700 IF ¬NULL(IMPS←CDR IMPS) THEN GO LOOP1;
02800 LOOP2:IF NULL PREMS THEN RETURN CAR RES;
02900 IF ¬MEMBER(CAR PREMS,ANTECEDS) THEN ERREND '(UNPROVEN DISJUNCT);
03000 PREMS←CDR PREMS;
03100 GO LOOP2;
03200 END;
03300
00100 EXPR PCERR;
00200 BEGIN PRINT 'PROOF!-CHECKER ;
00300 LINELENGTH CONSOLEWIDTH;
00400 OFF FILEPRINT;
00500 ON PRINT;
00600 OFF TWODIM;
00700 EVAL '(BEGIN);
00800 END;
00900
01000 EXPR PCINIT; BEGIN EXCISE();
01100 ONDD();
01200 INITOPS();
01300 INITALL();
01400 INITFN 'PCSTART ;
01500 PRINT 'PROOF-CHECKER-INITIALIZED ;
01600 END;
01700
01800 EXPR PCSTART; BEGIN ERRSET(RESTOREALL(PCHECK.INI),NIL);
01900 INITFN 'PCERR ;
02000 PCERR();
02100 END;
02200
02300 EXPR PAIRLIS(CARS,CDRS);
02400 IF NULL CARS ∨ NULL CDRS THEN NIL
02500 ELSE (CAR CARS.CAR CDRS).PAIRLIS(CDR CARS,CDR CDRS);
02600
02700 EXPR QUANTEQUIV(EXP1,CONT1,EXP2,CONT2);
02800 BEGIN SCALAR GEN,TEM;
02900 IF ATOM EXP1 THEN GO ATOM;
03000 IF ATOM CAR EXP1 THEN GO FUN;
03100 IF ISQUANT CAAR EXP1 THEN GO QUANT;
03200 LIST: IF NULL EXP1 THEN RETURN NULL EXP2;
03300 IF ¬QUANTEQUIV(CAR EXP1,CONT1,CAR EXP2,CONT2) THEN RETURN NIL;
03400 EXP1←CDR EXP1;
03500 EXP2←CDR EXP2;
03600 GO LIST;
03700 ATOM: TEM←ASSOC(EXP1,CONT1);
03800 IF ¬NULL TEM THEN EXP1←CDAR TEM;
03900 TEM←ASSOC(EXP2,CONT2);
04000 IF ¬NULL TEM THEN EXP1←CDAR TEM;
04100 RETURN EXP1=EXP2;
04200 FUN: IF CAR EXP1≠CAR EXP2 THEN RETURN NIL;
04300 EXP1←CDR EXP1;
04400 EXP2←CDR EXP2;
04500 GO LIST;
04600 QUANT:IF ¬ISQUANT CAAR EXP2 ∨ CAAR EXP1≠CAAR EXP2 THEN RETURN NIL;
04700 GEN←GENSYM();
04800 RETURN QUANTEQUIV(CADR EXP1,(CADAR EXP1.GEN).CONT1,
04900 CADR EXP2,(CADAR EXP2.GEN).CONT2);
05000 END;
05100
00100 EXPR PROPSUBST(TERM,VAR,EXP);
00200 PROPSUBST1(TERM,VAR,EXP,MAKERNL(FREEVARS TERM,ALLVARS EXP));
00300
00400 EXPR PROPSUBST1(TERM,VAR,EXP,RNL);
00500 IF ATOM EXP
00600 THEN IF ISVAR EXP
00700 THEN IF EXP=VAR THEN TERM ELSE EXP
00800 ELSE EXP
00900 ELSE IF ¬ATOM CAR EXP ∧ ISQUANT CAAR EXP
01000 THEN BEGIN SCALAR NEWNAM;
01100 NEWNAM←ASSOC(CADAR EXP,RNL);
01200 NEWNAM←IF NULL NEWNAM
01300 THEN CADAR EXP
01400 ELSE CDR NEWNAM;
01500 RETURN LIST(LIST(CAAR EXP,NEWNAM),
01600 PROPSUBST1(TERM,
01700 VAR,
01800 SUBST(NEWNAM,
01900 CADAR EXP,
02000 CADR EXP),
02100 RNL));
02200 END
02300 ELSE PROPSUBST1(TERM,VAR,CAR EXP,RNL)
02400 .PROPSUBSTL(TERM,VAR,CDR EXP,RNL);
02500
02600 EXPR PROPSUBSTL(TERM,VAR,EXPL,RNL);
02700 IF NULL EXPL THEN NIL ELSE
02800 PROPSUBST1(TERM,VAR,CAR EXPL,RNL).PROPSUBSTL(TERM,VAR,CDR EXPL,RNL);
02900
00100 EXPR REPEITHER(WFF,EQUAT,FLAG,ORD);
00200 IF ¬ISEQUIVALENCE CAR EQUAT THEN ERREND '(NO EQUATION)
00300 ELSE REPNTH(IF FLAG THEN CADDR EQUAT ELSE CADR EQUAT,
00400 IF FLAG THEN CADR EQUAT ELSE CADDR EQUAT,
00500 WFF,
00600 ORD);
00700
00800 EXPR REPNTH(NEW,OLD,EXP,NUM);
00900 BEGIN SCALAR NEWEXP,ORDCNT;
01000 ORDCNT←0;
01100 NEWEXP←REPNTH1(NEW,OLD,EXP,NIL,NUM);
01200 IF ORDCNT<NUM THEN ERREND '(NO REPLACEMENT);
01300 RETURN NEWEXP;
01400 END;
01500
01600 EXPR REPNTH1(NEXP,OEXP,EXP,CON,NUM);
01700 BEGIN SCALAR BVAR,GEN,NVAR;
01800 IF QUANTEQUIV(OEXP,NIL,EXP,CON) THEN GO GOTIT;
01900 IF ATOM EXP THEN RETURN EXP;
02000 IF ATOM CAR EXP THEN RETURN CAR EXP
02100 .REPNTHL(NEXP,OEXP,CDR EXP,CON,NUM);
02200 IF ISQUANT CAAR EXP THEN GO QUANT;
02300 QUANT:GEN←GENSYM();
02400 BVAR←CADAR EXP;
02500 NVAR←IF BVARεALLVARS NEXP
02600 THEN MAKEVAR(BVAR,ALLVARS CADR EXP)
02700 ELSE BVAR;
02800 RETURN LIST(LIST(CAAR EXP,NVAR),
02900 REPNTH1(NEXP,
03000 OEXP,
03100 SUBST(NVAR,BVAR,CADR EXP),
03200 (NVAR.GEN).CON,
03300 NUM));
03400 GOTIT:ORDCNT←ORDCNT+1;
03500 RETURN IF ORDCNT=NUM THEN NEXP ELSE EXP;
03600 END;
03700
03800 EXPR REPNTHL(NEXP,OEXP,LST,CON,NUM);
03900 IF NULL LST THEN NIL ELSE
04000 REPNTH1(NEXP,OEXP,CAR LST,CON,NUM).REPNTHL(NEXP,OEXP,CDR LST,CON,NUM);
04100
00100 EXPR SAVEAXIOM AXIOM;
00200 PRINTEXPR LIST('ADDAXIOM,AXIOM,GET(AXIOM,'AXIOM));
00300
00400 EXPR SAVEAXCOM AXIOM;
00500 PRINTEXPR LIST('GIVEAX,AXIOM,GET(AXIOM,'AXIOM));
00600
00700 EXPR SAVEPRFCOM PROOF;
00800 BEGIN SCALAR PRF;
00900 PRINT LIST('PROOF,PROOF);
01000 PRF←GET(PROOF,'PROOF);
01100 LOOP: IF NULL PRF THEN RETURN TERPRI();
01200 IF CAR CADDR CAR PRF='USETHM THEN SAVETHMCOM CADR CADDR CAR PRF;
01300 PRINT CAAR PRF;
01400 PRINC '! ;
01500 PRINTSUBEXPR(CADDR CAR PRF,9,0);
01600 PRF←CDR PRF;
01700 GO LOOP;
01800 END;
01900
02000 EXPR SAVEPROOF PROOF;
02100 PRINTEXPR LIST('GIVEPROOF,PROOF,GET(PROOF,'PROOF));
02200
02300 EXPR SAVESCHEMA SCHEMA;
02400 PRINTEXPR LIST('ADDSCHEMA,SCHEMA,GET(SCHEMA,'SCHEMA));
02500
02600 EXPR SAVESCHMCOM SCHEMA;
02700 PRINTEXPR LIST('GIVESCHM,SCHEMA,GET(SCHEMA,'SCHEMA));
02800
02900 EXPR SAVETHEOREM THEOREM;
03000 PRINTEXPR LIST('ADDTHM,
03100 THEOREM,
03200 CAR GET(THEOREM,'BY),
03300 CADR GET(THEOREM,'BY));
03400
03500 EXPR SAVETHMCOM THEOREM;
03600 PRINTEXPR LIST('MAKETHM,
03700 THEOREM,
03800 CAR GET(THEOREM,'BY),
03900 CADR GET(THEOREM,'BY));
04000 EXPR SETDIF(X,Y);
04100 BEGIN SCALAR ANS;
04200 LOOP: IF NULL X THEN RETURN REVERSE ANS;
04300 IF NOT MEMBER(CAR X,Y) THEN ANS←CAR X.ANS;
04400 X←CDR X;
04500 GO LOOP;
04600 END;
04700
00100 EXPR SHOWAXIOM NAME;
00200 BEGIN PRINT 'AXIOM ;
00300 PRINC NAME;
00400 TERPRI();
00500 SHOWEXP GET(NAME,'AXIOM);
00600 TERPRI();
00700 END;
00800
00900 EXPR SHOWCURLINE; IF CURLINE()=0 THEN SHOW() ELSE SHOWLINE GETCURLINE();
01000
01100 EXPR SHOWEXP EXP; IF !*TWODIM THEN TDDEXP(EXP,CURCOL(),0) ELSE INFX EXP;
01200
01300 EXPR SHOWLINE(LINTXT);
01400 BEGIN SCALAR COM;
01500 TERPRI(); TERPRI();
01600 PRINC CAR LINTXT;
01700 PRINC '!: ;PRINC '! ;
01800 SHOWEXP CADR LINTXT;
01900 PRINS 'BY ;
02000 COM←CADDR LINTXT;
02100 IF CAR COM = 'ASS THEN GO ASS;
02200 IF CAR COM='USEAX THEN COM←'AXIOM.CDR COM;
02300 IF CAR COM='USESCHM THEN COM←'SCHEMA.CDR COM;
02400 IF CAR COM='USETHM THEN COM←'THEOREM.CDR COM;
02500 SHOWEXP COM;
02600 IF NULL CADDDR LINTXT THEN RETURN;
02700 PRINS 'ASSUMING ;
02800 PRINS CADDDR LINTXT;
02900 RETURN;
03000 ASS: PRINS 'ASSUMPTION ;
03100 END;
03200
00100 EXPR SHOWPROOF(NAME);
00200 BEGIN PRINT 'PROOF ;
00300 PRINS NAME;
00400 MAPC(FUNCTION SHOWLINE,GET(NAME,'PROOF));
00500 TERPRI();
00600 END;
00700
00800 EXPR SHOWSCHEMA(NAME);
00900 BEGIN PRINT 'SCHEMA ;
01000 PRINC NAME;
01100 TERPRI();
01200 SHOWEXP GET(NAME,'SCHEMA);
01300 TERPRI();
01400 END;
01500
01600 EXPR SHOWTHEOREM(NAME);
01700 BEGIN PRINT 'THEOREM ;
01800 PRINS NAME;
01900 TERPRI();
02000 SHOWEXP GET(NAME,'THEOREM);
02100 END;
02200
02300 DEFPROP(AXIOM,SHOWAXIOM,IMAGE);
02400 DEFPROP(PROOF,SHOWPROOF,IMAGE);
02500 DEFPROP(SCHEMA,SHOWSCHEMA,IMAGE);
02600 DEFPROP(THEOREM,SHOWTHEOREM,IMAGE);
02700
02800 EXPR SPECALL(FORM,ARGS);
02900 BEGIN
03000 LOOP: IF NULL ARGS THEN RETURN FORM;
03100 IF ATOM FORM THEN ERREND '(ATOMIC EXPRESSION);
03200 IF CAAR FORM≠'FORALL ∧CAAR FORM≠'THEREEXISTS THEN
03300 ERREND '(NOT QUANTIFIED EXPRESSION);
03400 RETURN SPECALL(PROPSUBST(CAR ARGS,CADAR FORM,CADR FORM),CDR ARGS);
03500 END;
03600
00100 EXPR TH1(A1,A2,A,C);
00200 IF NULL A
00300 THEN TH2(A1,A2,NIL,NIL,C)
00400 ELSE CAR AεC∨IF ATOM CAR A
00500 THEN TH1(IF CAR AεA1 THEN A1 ELSE CAR A.A1,A2,CDR A,C)
00600 ELSE TH1(A1,IF CAR AεA2 THEN A2 ELSE CAR A.A2,CDR A,C);
00700
00800 EXPR TH2(A1,A2,C1,C2,C);
00900 IF NULL C THEN TH(A1,A2,C1,C2)
01000 ELSE IF ATOM CAR C
01100 THEN TH2(A1,A2,IF CAR CεC1 THEN C1 ELSE CAR C.C1,C2,CDR C)
01200 ELSE TH2(A1,A2,C1,IF CAR CεC2 THEN C2 ELSE CAR C.C2,CDR C);
01300
01400 EXPR TH(A1,A2,C1,C2);
01500 IF NULL A2
01600 THEN ¬NULL C2 ∧ THR(CAR C2,A1,A2,C1,CDR C2)
01700 ELSE THL(CAR A2,A1,CDR A2,C1,C2);
01800
01900 EXPR THL(U,A1,A2,C1,C2);
02000 IF CAR U='NOT THEN TH1R(CADR U,A1,A2,C1,C2) ELSE
02100 IF CAR U='AND THEN TH2L(CDR BINAND CDR U,A1,A2,C1,C2) ELSE
02200 IF CAR U='OR THEN TH1L(CADR BINOR CDR U,A1,A2,C1,C2)
02300 ∧TH1L(CADDR BINOR CDR U,A1,A2,C1,C2) ELSE
02400 IF CAR U='IMPLIES THEN TH1L(CADDR U,A1,A2,C1,C2)
02500 ∧TH1R(CADR U,A1,A2,C1,C2) ELSE
02600 IF CAR U='EQUIVALENT THEN TH2L(CDR U,A1,A2,C1,C2)
02700 ∧TH2R(CDR U,A1,A2,C1,C2) ELSE
02800 IF UεC1 THEN T ELSE TH(U.A1,A2,C1,C2);
02900
03000 EXPR THR(U,A1,A2,C1,C2);
03100 IF CAR U='NOT THEN TH1L(CADR U,A1,A2,C1,C2) ELSE
03200 IF CAR U='AND THEN TH1R(CADR U,A1,A2,C1,C2)
03300 ∧TH1R(CADDR U,A1,A2,C1,C2) ELSE
03400 IF CAR U='OR THEN TH2R(CDR U,A1,A2,C1,C2) ELSE
03500 IF CAR U='IMPLIES THEN TH11(CDR U,A1,A2,C1,C2) ELSE
03600 IF CAR U='EQUIVALENT THEN TH11(CDR U,A1,A2,C1,C2)
03700 ∧TH11(REVERSE CDR U,A1,A2,C1,C2) ELSE
03800 IF UεA1 THEN T ELSE TH(A1,A2,U.C1,C2);
03900
00100 EXPR TH1L(V,A1,A2,C1,C2);
00200 IF ATOM V THEN VεC1∨TH(V.A1,A2,C1,C2) ELSE VεC2∨TH(A1,V.A2,C1,C2);
00300
00400 EXPR TH1R(V,A1,A2,C1,C2);
00500 IF ATOM V THEN VεA1∨TH(A1,A2,V.C1,C2) ELSE VεA2∨TH(A1,A2,C1,V.C2);
00600
00700 EXPR TH2L(V,A1,A2,C1,C2);
00800 IF ATOM CAR V
00900 THEN CAR VεC1∨TH1L(CADR V,CAR V.A1,A2,C1,C2)
01000 ELSE CAR VεC2∨TH1L(CADR V,A1,CAR V.A2,C1,C2);
01100
01200 EXPR TH2R(V,A1,A2,C1,C2);
01300 IF ATOM CAR V
01400 THEN CAR VεA1∨TH1R(CADR V,A1,A2,CAR V.C1,C2)
01500 ELSE CAR VεA2∨TH1R(CADR V,A1,A2,C1,CAR V.C2);
01600
01700 EXPR TH11(V,A1,A2,C1,C2);
01800 IF ATOM CAR V
01900 THEN CAR VεC1∨TH1R(CADR V,CAR V.A1,A2,C1,C2)
02000 ELSE CAR VεC2∨TH1R(CADR V,A1,CAR V.A2,C1,C2);
02100
00100 EXPR UNGEN(WFF,ASS,FVAR,BVAR);
00200 BEGIN SCALAR WFF,TEM;
00300 IF FREEIN(FVAR,ASS) THEN ERREND '(VARIABLE FREE IN ASSUMPTIONS);
00400 IF USEDINEXISTSPEC FVAR THEN
00500 ERREND '(USED IN EXISTENTIALLY SPECIFIED LINE);
00600 TEM←GENSYM();
00700 WFF←SUBST(TEM,FVAR,WFF);
00800 IF BVARεALLVARS WFF THEN ERREND '(VARIABLE CONFLICT);
00900 RETURN LIST(LIST('FORALL,BVAR),SUBST(BVAR,TEM,WFF));
01000 END;
01100
01200 EXPR UNION SETS;
01300 IF NULL SETS THEN NIL ELSE
01400 IF NULL CDR SETS THEN CAR SETS ELSE
01500 UNION2(CAR SETS,UNION CDR SETS);
01600
01700 EXPR UNION2(SET1,SET2);
01800 IF NULL SET1 THEN SET2 ELSE
01900 IF MEMBER(CAR SET1,SET2) THEN UNION2(CDR SET1,SET2) ELSE
02000 UNION2(CDR SET1,CAR SET1.SET2);
02100
00100 EXPR USEDINEXISTSPEC VAR;
00200 BEGIN SCALAR PRF;
00300 PRF←CURTEXT();
00400 LOOP: IF NULL PRF THEN RETURN NIL;
00500 IF CAR CADDAR PRF='ES AND VARεFREEVARS CADAR PRF THEN RETURN T;
00600 PRF←CDR PRF;
00700 GO LOOP;
00800 END;
00900
01000 EXPR USEDVAR VAR;
01100 BEGIN SCALAR PRF;
01200 PRF←CURTEXT();
01300 LOOP: IF NULL PRF THEN RETURN NIL;
01400 IF VARεALLVARS CADAR PRF THEN RETURN T;
01500 PRF←CDR PRF;
01600 GO LOOP;
01700 END;
01800
01900 EXPR VALID PROP; PROP ≠ 'INVALID ;
02000
02100 EXPR WFFLIST L; MAPCAR(FUNCTION WFFPART,L);
02200
02300 EXPR WFFPART LINE; CADR GETLINE LINE;
02400
00100 %INFIX PRINTING ROUTINES%
00200
00300 EXPR GETINFXNAM ATOM;
00400 BEGIN SCALAR NAME;
00500 IF NUMBERP ATOM THEN RETURN ATOM;
00600 NAME←SEEKPROP(ATOM,'INFXNAM);
00700 IF ¬NULL NAME THEN RETURN PROPVAL NAME;
00800 RETURN ATOM;
00900 END;
01000
01100 EXPR INFX(EXP); BEGIN INFXEXPR(EXP,0,0); INFXATOM '! ; END;
01200
01300 EXPR INFXARGS(ARGS,LPREC,RPREC);
01400 IF NULL ARGS THEN BEGIN INFXATOM '!( ; INFXATOM '!) ; END ELSE
01500 IF NULL CDR ARGS THEN
01600 BEGIN INFXATOM '! ; INFXEXPR(CAR ARGS,LPREC,RPREC); END ELSE
01700 INFXPARENED('!*COMMA!*.ARGS,LPREC,RPREC);
01800
01900 PUTPROP('INFXATOM,'PRNTATOM,'EXPR);
02000
02100 EXPR INFXCOND(S,L,R);
02200 BEGIN INFXATOM 'IF ;INFXATOM '! ;
02300 INFXEXPR(CAADR S,0,0); INFXATOM '! ;
02400 INFXATOM 'THEN ; INFXATOM '! ;
02500 INFXEXPR(CADADR S,0,0); INFXATOM '! ;
02600 IF NULL CDDR S THEN RETURN;
02700 INFXATOM 'ELSE ; INFXATOM '! ;
02800 INFXEXPR(CADR CADDR S,0,0);
02900 END;
03000
03100 EXPR INFXFUN(FN,LPREC,RPREC);
03200 IF ATOM FN THEN INFXATOM FN ELSE INFXPARENED(FN,LPREC,RPREC);
03300
03400 EXPR INFXEXPR(EXP,LPREC,RPREC);
03500 BEGIN SCALAR OP;
03600 IF ATOM EXP THEN RETURN INFXATOM EXP;
03700 IF ¬ATOM CAR EXP THEN GO NOATM;
03800 OP←GETGET(CAR EXP,'INFXFUN);
03900 IF ¬NULL OP THEN RETURN APPLY(PROPVAL OP,LIST(EXP,LPREC,RPREC));
04000 NOATM:INFXFUN(CAR EXP,LPREC,RPREC);
04100 INFXARGS(CDR EXP,10000,RPREC);
04200 END;
04300
00100 EXPR INFXLIST(OP,ARGS,LPREC,RPREC);
00200 BEGIN SCALAR PREC;
00300 PREC←GET(OP,'PREC);
00400 LOOP: IF NULL ARGS THEN RETURN;
00500 INFXATOM OP;
00600 INFXEXPR(CAR ARGS,
00700 CADR PREC,
00800 IF NULL CDR ARGS THEN RPREC ELSE CAR PREC);
00900 ARGS←CDR ARGS;
01000 GO LOOP;
01100 END;
01200
01300 EXPR INFXOPER(EXP,LPREC,RPREC);
01400 BEGIN SCALAR PREC;
01500 PREC←GET(CAR EXP,'PREC);
01600 IF CAR PREC<LPREC ∨ CADR PREC<RPREC THEN
01700 RETURN INFXPARENED(EXP,LPREC,RPREC);
01800 IF NULL CDR EXP THEN RETURN INFXATOM CAR EXP;
01900 IF NULL CDDR EXP THEN RETURN INFXLIST(CAR EXP,CDR EXP,LPREC,RPREC);
02000 INFXEXPR(CADR EXP,LPREC,CAR PREC);
02100 RETURN(INFXLIST(CAR EXP,CDDR EXP,LPREC,RPREC));
02200 END;
02300
02400 EXPR INFXPARENED(EXP,LPREC,RPREC);
02500 BEGIN INFXATOM '!( ; INFXEXPR(EXP,0,0); INFXATOM '!) ; END;
02600
02700 EXPR INFXQUOTE(SEXPR,LPREC,RPREC);
02800 BEGIN INFXATOM 'QUOTE ;PRIN1 CADR SEXPR; END;
02900
03000 EXPR INFXSPEC(SEXPR,LPREC,RPREC);
03100 GET(CAR SEXPR,'SPECOPER)(SEXPR,LPREC,RPREC);
03200
03300 EXPR PRNTATOM AT;
03400 BEGIN SCALAR NAM;
03500 NAM←GETINFXNAM AT;
03600 IF CHRCT()<FLATSIZE NAM+1 THEN TERPRI();
03700 PRINC NAM;
03800 END;
03900
04000 PUTPROP('PREC,'INFXOPER,'INFXFUN);
04100 PUTPROP('SPECOPER,'INFXSPEC,'INFXFUN);
04200
04300 PUTPROP('COND,'INFXCOND,'SPECOPER);
04400 PUTPROP('QUOTE,'INFXQUOTE,'SPECOPER);
04500
04600 %END%
04700
00100 %TWO DIMENSIONAL DISPLAY ROUTINES%
00200
00300 EXPR FITSLINE(EXP,COL,PARS);
00400 BEGIN SCALAR ANS,EXPEXP,EXPLGTH,EXPLIM;
00500 IF ATOM EXP THEN RETURN T;
00600 EXPLGTH←0;
00700 EXPEXP←EXP;
00800 EXPLIM←LINELENGTH NIL-(COL+PARS);
00900 INITPROP('INFXATOM,'LGTHATOM,'EXPR);
01000 ANS←ERRSET INFXEXPR(EXPEXP,1,0);
01100 DELETEPROP('INFXATOM,'EXPR);
01200 RETURN ANS;
01300 END;
01400
01500 EXPR LGTHATOM AT;
01600 BEGIN EXPLGTH←EXPLGTH+FLATSIZE GETINFXNAM AT;
01700 IF EXPLGTH≤EXPLIM THEN RETURN;
01800 EXPLGTH←NIL;
01900 ERR();
02000 END;
02100
02200 EXPR TDD EXP; TDDEXP(EXP,1,0);
02300
02400 EXPR TDDARGS(ARGS,COL,PARS);
02500 IF ¬NULL ARGS∧NULL CDR ARGS THEN
02600 BEGIN PRINC '! ; TDDEXP(CAR ARGS,COL+1,PARS); END ELSE
02700 BEGIN INFXATOM '!( ; TDDLIST(ARGS,COL+1,PARS+1); INFXATOM '!) ; END;
02800
02900 EXPR TDDEXP(EXP,COL,PARS);
03000 BEGIN SCALAR TEM;
03100 TABTO COL;
03200 IF FITSLINE(EXP,COL,PARS) THEN RETURN INFXEXPR(EXP,0,0);
03300 TEM←GETGET(CAR EXP,'TDDFUN);
03400 IF ¬NULL TEM THEN RETURN APPLY(PROPVAL TEM,LIST(EXP,COL,PARS));
03500 NOAT: TDDFUNC(CAR EXP,COL,PARS);
03600 TDDARGS(CDR EXP,CURCOL(),PARS);
03700 END;
03800
03900 EXPR TDDFUNC(EXP,COL,PARS);
04000 BEGIN IF ATOM EXP THEN RETURN INFXATOM EXP;
04100 INFXATOM '!( ;
04200 TDDEXP(EXP,COL+1,PARS+1);
04300 INFXATOM '!) ;
04400 END;
04500
00100 EXPR TDDLIST(EXP,COL,PARS);
00200 BEGIN
00300 LOOP: IF NULL EXP THEN RETURN NIL;
00400 TDDEXP(CAR EXP,COL,PARS+1);
00500 EXP←CDR EXP;
00600 IF ¬NULL EXP THEN INFXATOM '!, ;
00700 GO LOOP;
00800 END;
00900
01000 EXPR TDDINFX(EXP,COL,PARS);
01100 BEGIN SCALAR ARGS,INCR,OP;
01200 IF NULL CDR EXP ∨ NULL CDDR EXP THEN RETURN INFX EXP;
01300 OP←CAR EXP;
01400 INCR←FLATSIZE GETINFXNAM CAR EXP;
01500 TDDEXP(CADR EXP,COL,PARS);
01600 ARGS←CDDR EXP;
01700 LOOP: IF NULL ARGS THEN RETURN NIL;
01800 TERPRI();
01900 TABTO COL;
02000 INFXATOM OP;
02100 TDDEXP(CAR ARGS,COL+INCR,PARS);
02200 ARGS←CDR ARGS;
02300 GO LOOP;
02400 END;
02500
02600 PUTPROP('PREC,'TDDINFX,'TDDFUN);
02700
02800 %END%
02900
00100 %S-EXPRESSION PRINTING ROUTINES%
00200
00300 EXPR ALLFIT(LIST,WIDTH,RPARS);
00400 BEGIN IF NULL LIST THEN RETURN T;
00500 LOOP: IF NULL CDR LIST THEN RETURN FLATSIZE CAR LIST≤WIDTH-RPARS;
00600 IF FLATSIZE CAR LIST>WIDTH THEN RETURN NIL;
00700 LIST←CDR LIST;
00800 GO LOOP;
00900 END;
01000
01100 EXPR PRINL X;
01200 IF NULL X THEN NIL ELSE
01300 IF CHRCT()<FLATSIZE CAR X+2 THEN
01400 BEGIN TERPRI(); PRINC '! ; PRINL X; END ELSE
01500 BEGIN PRINS CAR X; PRINL CDR X; END;
01600
01700 EXPR PRINS X; BEGIN PRINC X; PRINC '! ; END;
01800
01900 EXPR PRINTEXPR EXP; BEGIN PRINTSUBEXPR(EXP,1,0); TERPRI(); TERPRI(); END;
02000
02100 EXPR PRINTLIST(LIST,LMARG,RPARS);
02200 BEGIN PRINC '!( ;
02300 PRINTMEMBERS(LIST,LMARG+1,RPARS+1);
02400 PRINC '!) ;
02500 END;
02600
02700 EXPR PRINTMEMBERS(LIST,LMARG,RPARS);
02800 BEGIN
02900 LOOP: IF NULL LIST THEN RETURN NIL;
03000 IF ATOM LIST THEN RETURN
03100 BEGIN PRINC '! !.! ; PRIN1 LIST; END;
03200 PRINTSUBEXPR(CAR LIST,
03300 LMARG,
03400 IF NULL CDR LIST THEN RPARS+1 ELSE
03500 IF ATOM CDR LIST THEN RPARS+4 ELSE 0);
03600 LIST←CDR LIST;
03700 GO LOOP;
03800 END;
03900
00100 EXPR PRINTSUBEXPR(SEXPR,LMARG,RPARS);
00200 BEGIN SCALAR TEM;
00300 TABTO LMARG;
00400 IF ATOM SEXPR THEN RETURN PRIN1 SEXPR;
00500 IF ATOM CAR SEXPR ∧ ¬NUMBERP CAR SEXPR
00600 THEN TEM←GETGET(CAR SEXPR,'PPROP);
00700 IF ¬NULL TEM THEN RETURN (PROPVAL TEM)(SEXPR,LMARG,RPARS);
00800 IF FLATSIZE SEXPR ≤ CHRCT()-RPARS THEN RETURN PRIN1 SEXPR;
00900 IF FLATSIZE CAR SEXPR≤4∨ALLFIT(CDR SEXPR,
01000 CHRCT()-(2+FLATSIZE CAR SEXPR),
01100 RPARS)
01200 THEN RETURN BEGIN PRINC '!( ; PRIN1 CAR SEXPR; PRINC '! ;
01300 PRINTMEMBERS(CDR SEXPR,CURCOL(),1+RPARS);
01400 PRINC '!) ;
01500 END;
01600 PRINTLIST(SEXPR,LMARG,RPARS);
01700 END;
01800
01900 EXPR PRINTN(CHAR,NUM);
02000 BEGIN SCALAR NO;
02100 NO←1;
02200 LOOP: IF NUM<NO THEN RETURN NUM;
02300 PRINC CHAR;
02400 NO←NO+1;
02500 GO LOOP;
02600 END;
02700
02800 EXPR PRINTNOCRFUN(SEXPR,LMARG,RPARS);
02900 BEGIN IF FLATSIZE SEXPR ≤ CHRCT()-RPARS THEN RETURN PRIN1 SEXPR;
03000 PRINC '!( ;
03100 PRIN1 CAR SEXPR;
03200 PRINC '! ;
03300 PRINC CADR SEXPR;
03400 PRINTMEMBERS(CDDR SEXPR,LMARG+1,RPARS+1);
03500 PRINC '!) ;
03600 END;
03700
03800 EXPR TABTO COLNO;
03900 BEGIN IF CURCOL()>COLNO THEN TERPRI();
04000 PRINTN('! ,LSH(COLNO-CURCOL(),-3));
04100 PRINTN('! ,COLNO-CURCOL());
04200 END;
04300
04400 PUTPROP('NOCR,'PRINTNOCRFUN,'PPROP);
04500
04600 FLAG('(ADDAXIOM ADDSCHEMA ADDTHEOREM DEFPROP GIVEAX GIVEPROOF GIVESCHM
04700 MAKETHM SETQ USEAX USESCHM),
04800 'NOCR);
04900
05000 %END%
05100
00100 PROG2(PRECLIS!*←'IMPLIES.PRECLIS!*,MKPREC());
00200 PROG2(PRECLIS!*←'EQUIVALENT.PRECLIS!*,MKPREC());
00300
00400 PRECSET('CMAPS,'LESSP);
00500 PRECSET('CONTAINED,'LESSP);
00600 PRECSET('INTERSECTION,'CONTAINED);
00700 PRECSET('MAPS,'INTERSECTION);
00800 PRECSET('MEMBER,'LESSP);
00900 PRECSET('PRODUCT,'INTERSECTION);
01000 PRECSET('UNION,'CONTAINED);
01100
01200 PUTPROP('!&,'(NIL AND NIL),'SWITCH!*);
01300 PUTPROP('!⊂,'(NIL CONTAINED NIL),'SWITCH!*);
01400 PUTPROP('!=,'(> EQUAL IMPLIES),'SWITCH!*);
01500 PUTPROP('!≡,'(NIL EQUIVALENT NIL),'SWITCH!*);
01600 PUTPROP('!∀,'(NIL FORALL NIL),'SWITCH!*);
01700 PUTPROP('!≥,'(NIL GEQ NIL),'SWITCH!*);
01800 PUTPROP('!∩,'(NIL INTERSECTION NIL),'SWITCH!*);
01900 PUTPROP('!→,'(→ MAPS CMAPS),'SWITCH!*);
02000 PUTPROP('!⊃,'(NIL IMPLIES NIL),'SWITCH!*);
02100 PUTPROP('!≤,'(NIL LEQ NIL),'SWITCH!*);
02200 PUTPROP('!ε,'(NIL MEMBER NIL),'SWITCH!*);
02300 PUTPROP('!≠,'(NIL NEQ NIL),'SWITCH!*);
02400 PUTPROP('!⊗,'(NIL PRODUCT NIL),'SWITCH!*);
02500 PUTPROP('!∃,'(NIL THEREEXISTS NIL),'SWITCH!*);
02600 PUTPROP('!∪,'(NIL UNION NIL),'SWITCH!*);
02700
02800 PUTPROP('ALL,'FORALL,'NEWNAM);
02900 PUTPROP('EXISTS,'THEREEXISTS,'NEWNAM);
03000 PUTPROP('EQU,'EQUIVALENT,'NEWNAM);
03100 PUTPROP('GREATEQ,'GEQ,'NEWNAM);
03200 PUTPROP('IMP,'IMPLIES,'NEWNAM);
03300 PUTPROP('LESSEQ,'LEQ,'NEWNAM);
03400 PUTPROP('MEM,'MEMBER,'NEWNAM);
03500
03600 LETTER 3; %makes the letter beta an atom constituent%
03700
00100 REMPROP('LAMBDA,'STAT);
00200 REMPROP('GO,'STAT);
00300 REMPROP('STEP,'DELIM);
00400 REMPROP('DO,'DELIM);
00500
00600 REMPROP('MAP,'NEWFORM);
00700 REMPROP('MAPLIST,'NEWFORM);
00800 REMPROP('MAPCAR,'NEWFORM);
00900
01000 REMPROP('EXPLODE,'NEWNAM);
01100
01200 PUTPROP('EXPR,'PROCDEF,'STAT);
01300
01400 LOGICALCONSTANTS ← '(TRUE FALSE);
01500 QUANTIFIERS←'(FORALL LAMBDA THEREEXISTS);
01600
01700 DDWIDTH←84;
01800 FILEWIDTH←69;
01900 IIIWIDTH←88;
02000 IMLACWIDTH←80;
02100 TTYWIDTH←71;
02200
02300 SHUT PCHECK.LSP;
02400
02500 END;